\section{Related Work}
\label{sec:DRW}

Petri Nets and their declinations like Colored \textsc{Pn} (\textsc{Cpn}s), are widely used for formalizing systems' behavior and analyzing their relevant properties. However from an \textsc{Mde} point of view, translating complex models into \textsc{Apn}s is easier, because the gap for encoding the necessary data structures a engineer is working with is smaller due to the richness of algebraic specifications. However, a very restricted list of contributions investigated invariant preservation in \textsc{Pn}s.

%Given the simple graphical representation, expressiveness and analysability of
%Petri nets, many authors have published results on property preserving
%transformations for Petri nets. There is however a restricted list of authors
%who have investigated the subject of invariant preservation in algebraic or
%coloured Petri nets.


Padberg, together with several other co-authors, published extensively on invariant preservation of \textsc{Apn}s, building a full categorical framework for \textsc{Apn}s rule-based refinements. Our contribution extends Padberg's result published in \cite{Padberg97refinementversus,Padberg98rule-basedrefinement} but as already mentioned, this result does not consider guard strengthening. To the best of our knowledge, Padberg's work on this topic has been discontinued after a last survey paper~\cite{DBLP:conf/dfg/PadbergU03} has been published on the topic in 2003.

%Padberg has extensively published with several co-authors on a categorical
%framework for property preserving rule-based refinements of Petri nets,
%applicable in particular to algebraic Petri nets. Our paper presents an
%extension to Padberg's result initially presented as a technical report of the
%University of Berlin~\cite{Padberg97refinementversus}, and later as a journal
%publication~\cite{Padberg98rule-basedrefinement}. As mentioned previously,
%Padberg's result does not consider guard strengthening. To the best of our
%knowledge Padberg's work on this topic has been discontinued after a last survey paper~\cite{DBLP:conf/dfg/PadbergU03} has been published on the topic in 2003.

Around 2000, Cheung and Lu \cite{Cheung:99} studied five classes of invariant-preserving transformations in \textsc{Cpn}s, namely Insertion, Elimination, Replacement, Composition and Decomposition. Most closer to our work are the Insertion and Replacement (of transitions) transformations: for the former, they obtain full preservation but at the price restraining the markings and preserving guards, instead of our strengthening; while the latter is directly related to our guard strengthening, although their result also consider removing adjacent transitions' arcs. Nevertheless, guard strengthening, a necessary iterative process for tackling iterative \textsc{Mde} development, is not explicitly considered. The authors later concentrated in Place/Transition \textsc{Pn}s rather than \textsc{Cpn}s \cite{Huang2004245,huang2012property}. Lewis' Ph.D \cite{lewis2002incremental} studied morphisms allowing behavior-preserving refinements, and in particular refinements through bi-simulation.


%Around the same period of time Cheung and Lu have published five classes of
%invariant preserving transformations on coloured Petri nets~\cite{Cheung:99}.
%Coloured Petri nets are structurally similar to algebraic Petri nets, except
%that for those nets data types are pre-defined and the operations of those types are not explicitly modelled. In~\cite{Cheung:99} the \emph{Insersion}
%transformation is the one that comes the closest to our proposal, although the
%hypotheses in the theorem granting invariant preservation consider guard
%preservation, but not strengthening. The \emph{Replacement-of-Transitions} is
%related to the part of our proof that only considers guard strengthening,
%although the authors consider guard modification in the sense of taking changes
%in adjacent arcs into consideration. They do not tackle explicit guard
%strengthening. Subsequent work from these authors such as in~\cite{Huang2004245} or very recently as a book in~\cite{huang2012property} concentrates on place/transition nets rather than on coloured nets.


%Lewis has devoted a part of his Ph.D. dissertation~\cite{lewis2002incremental} to the study of morphisms that allow behavior preserving refinements of coloured Petri nets. In particular the authors study refinements that allow the refined net to be bisimilar to the original net.

In the \textsc{Mde} community, iterative development is widely used and adopted, with several case studies demonstrating its relevance (cf. \eg Grau, Joseph, and Sagesser's work on an iterative lifecycle model completing the classical waterfall one \cite{10.1109/MS.2012.74}). Himsl \etal{} \cite{springerlink:10.1007/978-3-540-74469-6-51} proposed an iterative \mbox{(meta-)} modeling process for enterprise engineering, dealing with metamodels migrations with reflection back on previously designed instances. This is directly related to our engineering process, although their contribution is strictly syntactic, whereas our iterations concern also the behavior. Konrad \etal{} \cite{Konrad2007} proposed $\mathsf{i^2MAP}$, an \textsc{Uml}-based framework for incremental and iterative modeling and analysis process dedicated to embedded systems. Very close to our approach, they derive temporal logic formul\ae\xspace from natural language specifications to express goals, against which syntactic and behavioral consistencies are checked. Kumazawa and Tamai studied in \cite{4724568} an interesting semi-automated iterative development case called \emph{model fixing}: it consists in using counterexamples of a model-checker to enhance a model in order to make it satisfy a property, by only using previously checked properties, the original model and counterexamples, without sacrificing too much the original model's integrity. It however would require some additional work to adapt this technique for \textsc{Apn}s, which is richer than the labeled transitions systems extension they are using. Uzam and Zhou proposed in \cite{DBLP:dblp_journals/tsmc/UzamZ07} an iterative and "easy-to-use deadlock prevention policy" for Flexible Manufacturing Systems, based on reachability analysis on Petri Nets. At each iteration, supposing that an effective solution to deadlock prevention exists, they detect a bad marking that is further used to prevent its reachability of the system, by modifying the Net accordingly. Our work contrasts with theirs in the fact that we deal with \textsc{Apn}s, which are more expressive from an \textsc{Mde} perspective, and that our iterations are mathematically proven, whereas their methodology was proved not to be sound (cf. \cite{DBLP:dblp_journals/tsmc/LiL09} for counterexamples).


%In model-driven engineering community, iterative modeling is widely adopted and there are lots of examples and publications. Credit Suisse IT Switzerland recently introduced an iterative lifecycle model based on Rational Unified Process (RUP) in addition to the waterfall lifecycle model~\cite{10.1109/MS.2012.74}. Himsl \etal{} proposed an iterative modeling
%process by iteratively adapting meta- and instance- sub models for enterprise 
%engineering~\cite{springerlink:10.1007/978-3-540-74469-6-51}. Konrad \etal{} proposed an incremental and iterative goal-based UML modeling and analysis process on detecting errors in embedded system design~\cite{Konrad2007}. 

%Kumazawa \etal{} studied similar problem with ours, that how to fix the model (quite similar with model evolution) to satisfy given properties~\cite{4724568}. The authors proposed an iterative model fixing method with counterexamples. They apply Multi-Valued Transition Systems (extension of Labeled Transition System) to model the specification and define the properties by Linear Temporal Logic (LTL). When a counterexample is obtained during model checking, they evolve the model by merging the original model with an extended fixing sub model which enables the merged model counterexample-free. 




%Uzam and Zhou proposed an iterative synthesis approach to define deadlock prevention policy for flexible manufacturing systems \cite{DBLP:dblp_journals/tsmc/UzamZ07}. The authors apply ordinary Petri Net to model the system's behavioral properties, including liveness and boundedness. Then they divide the reachability graph (state space) into two parts: deadlock zone and live zone. If any first-met bad state (state that falls into deadlock zone) detected, the proposed method would iteratively evolve the Petri Net model by introducing new Control Place, with a certain number of tokens,  which would enforce the original model satisfies the constraint represented as place invariant. The process is also similar with our proposal, since the authors proposed to preserve the live zone of the reachability graph of the Petri Net model throughout the procedure, while our proposal is iteratively preserving properties represented as type invariant which benefits from algebraic data types. However, their work faced some problems because there is no sufficient formal proof for the theory. Li and Liu criticized Uzam and Zhou's work by giving a formal proof that Lemma 1 in \cite{DBLP:dblp_journals/tsmc/UzamZ07} is not always true \cite{DBLP:dblp_journals/tsmc/LiL09}. In contrast, we give the formal mathematical proof of our proposal, as mentioned before, by extending Padberg's work. 


% Padberg and Urb\'asek present in~\cite{DBLP:conf/dfg/PadbergU03} a survey
% on their complete work rule-based refinement of Petri nets. In that paper they
% present the theorem that place-preserving algebraic High-Level net morphisms are safety
% preserving, but their result is based on the hypothesis guards are
% unchanched, thus not strenghtened.
